//SIGNATURES

sig Calendar{
	hasOwner: one User,
	hasEvents: set Event
}

sig User{
	hasCalendar: one Calendar
}

abstract sig Event{
	hasOrganizer: one User,
	hasForecast: one WeatherCondition,
	desiredCondition: set WeatherCondition,
}

sig PersonalEvent extends Event{
	isInCalendar: one Calendar,
}

sig SharedEvent extends Event{
	hasParticipants: set User,
	isInCalendar: set Calendar
}

sig WeatherCondition{}

//FACTS

//hasOwner is the opposite of hascalendar
fact calendarsHaveOwners{
	all u: User, c: Calendar | (u = c.hasOwner) <=> (c = u.hasCalendar)
}

//hasEvent is the opposite of isInCalendar
fact eventsAreInCalendar{
	all s: SharedEvent, c: Calendar | (s in c.hasEvents) <=> (c in s.isInCalendar)
	all p: PersonalEvent, c: Calendar | (p in c.hasEvents) <=> (c = p.isInCalendar) 
}

//Shared events have to be both in their organizer and in their participants' calendar
fact sharedEventsAndCalendars{
	all s: SharedEvent, c: Calendar | (s in c.hasEvents) <=> ((c.hasOwner = s.hasOrganizer) or (c.hasOwner in s.hasParticipants))
}

//Personal events have to be in their organizer's calendar
fact personalEventsAndCalendars{
	all p: PersonalEvent, c: Calendar | (p in c.hasEvents) <=> (c.hasOwner = p.hasOrganizer)
}

//Organizer is still a participants
fact organizerIsAParticipant{
	all s: SharedEvent | s.hasOrganizer in s.hasParticipants
}

//Shared event, to be called like that, have more than one participant
fact sharedEventsHasMoreThanOneParticipant{
	all s: SharedEvent | #s.hasParticipants>1
}

//Each event must have at least one desired weather condition
fact atLeastOneDesiredWeather{
	all e: Event | #e.desiredCondition>0
}

//A weather condition must always be the forecast or the desired condition of an event
fact weatherConditionEvent{
	all e: Event, w1: WeatherCondition | no w: WeatherCondition | (w not in e.hasForecast and w not in e.desiredCondition) and w=w1
}

pred show(){}
run show for 4 but exactly 3 SharedEvent, exactly 4 User, exactly 2 WeatherCondition
